A:Realizer, k:Knd.
R-Feasible(A)
 isrcv(k)
 k  dom(R-da(A;source(lnk(k))))
 R-da(A;source(lnk(k)))(k)  Valtype(R-da(A;destination(lnk(k)));k) 

latex

Definitions	x:A. B(x), P  Q, t  T, x. t(x), f(x)?z, if b t else f fi, true, false, Prop, x(s), Feasible(D), P & Q, M(i), M.dout(l,tg), M.din(l,tg), SQType(T), {T}, , Unit, P  Q, A, False, Dsys, , Valtype(da;k)
Lemmas	R-Feasible-Dsys, assert wf, fpf-dom wf, Knd wf, Kind-deq wf, fpf-trivial-subtype-top, R-da wf, lsrc wf, lnk wf, isrcv wf, R-Feasible wf, es realizer wf, tagof wf, R-da-property, fpf-cap wf, rcv wf, ma-din wf, R-Dsys wf, ldst wf, top wf, isrcv-implies, Knd sq, bool wf, eqtt to assert, iff transitivity, bnot wf, not wf, eqff to assert, assert of bnot